\begin{tabbing}
$\forall$$A$, ${\it A'}$:Type.
\\[0ex]strong{-}subtype($A$;${\it A'}$)
\\[0ex]$\Rightarrow$ \=($\forall$$B$:($A$$\rightarrow$Type), ${\it eq}$:EqDecider(${\it A'}$), $f$, $g$:$a$:$A$ fp$\rightarrow$ $B$($a$), $x$:${\it A'}$, $P$, $Q$:($a$:$A$$\rightarrow$$B$($a$)$\rightarrow\mathbb{P}$).\+
\\[0ex]($\forall$$x$:$A$, $z$:$B$($x$). $P$($x$,$z$) $\Rightarrow$ $Q$($x$,$z$))
\\[0ex]$\Rightarrow$ $g$ $\subseteq$ $f$
\\[0ex]$\Rightarrow$ ($z$ != $f$($x$) $\Rightarrow$ $P$($x$,$z$))
\\[0ex]$\Rightarrow$ ($z$ != $g$($x$) $\Rightarrow$ $Q$($x$,$z$)))
\-
\end{tabbing}